\batchmode
\makeatletter
\def\input@path{{/Users/sergei.winitzki/Code/talks/ftt-fp/}}
\makeatother
\documentclass[english]{beamer}
\usepackage[T1]{fontenc}
\usepackage[latin9]{inputenc}
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{3}
\usepackage{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[all]{xy}
\ifx\hypersetup\undefined
  \AtBeginDocument{%
    \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
  }
\else
  \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
\fi

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
%% Because html converters don't know tabularnewline
\providecommand{\tabularnewline}{\\}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
 % this default might be overridden by plain title style
 \newcommand\makebeamertitle{\frame{\maketitle}}%
 % (ERT) argument for the TOC
 \AtBeginDocument{%
   \let\origtableofcontents=\tableofcontents
   \def\tableofcontents{\@ifnextchar[{\origtableofcontents}{\gobbletableofcontents}}
   \def\gobbletableofcontents#1{\origtableofcontents}
 }
 \newenvironment{lyxcode}
   {\par\begin{list}{}{
     \setlength{\rightmargin}{\leftmargin}
     \setlength{\listparindent}{0pt}% needed for AMS classes
     \raggedright
     \setlength{\itemsep}{0pt}
     \setlength{\parsep}{0pt}
     \normalfont\ttfamily}%
    \def\{{\char`\{}
    \def\}{\char`\}}
    \def\textasciitilde{\char`\~}
    \item[]}
   {\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usetheme[secheader]{Boadilla}
\usecolortheme{seahorse}
\title[Chapter 8: Applicative functors]{Chapter 8: Applicative functors and profunctors}
\subtitle{Part 2: Their laws and structure}
\author{Sergei Winitzki}
\date{2018-07-01}
\institute[ABTB]{Academy by the Bay}
\setbeamertemplate{headline}{} % disable headline at top
\setbeamertemplate{navigation symbols}{} % disable navigation bar at bottom
\usepackage[all]{xy}
\makeatletter
% Macros to assist LyX with XYpic when using scaling.
\newcommand{\xyScaleX}[1]{%
\makeatletter
\xydef@\xymatrixcolsep@{#1}
\makeatother
} % end of \xyScaleX
\makeatletter
\newcommand{\xyScaleY}[1]{%
\makeatletter
\xydef@\xymatrixrowsep@{#1}
\makeatother
} % end of \xyScaleY

\makeatother

\begin{document}
\frame{\titlepage}
\begin{frame}{Deriving the \texttt{\textcolor{blue}{\footnotesize{}ap}} operation
from \texttt{\textcolor{blue}{\footnotesize{}map2}} }

\vspace{-0.1cm}Can we avoid having to define $\text{map}_{n}$ separately
for each $n$?
\begin{itemize}
\item Use curried arguments, $\text{fmap}_{2}:(A\Rightarrow B\Rightarrow Z)\Rightarrow F^{A}\Rightarrow F^{B}\Rightarrow F^{Z}$
\item Set $A\equiv\left(B\Rightarrow Z\right)$ and apply $\text{fmap}_{2}$
to the identity $\text{id}^{\left(B\Rightarrow Z\right)\Rightarrow\left(B\Rightarrow Z\right)}$:
obtain $\text{ap}^{[B,Z]}:F^{B\Rightarrow Z}\Rightarrow F^{B}\Rightarrow F^{Z}\equiv\text{fmap}_{2}\left(\text{id}\right)$
\item The functions \texttt{\textcolor{blue}{\footnotesize{}fmap$_{2}$}}
and \texttt{\textcolor{blue}{\footnotesize{}ap}} are computationally
equivalent:{\footnotesize{}
\[
\text{fmap}_{2}\,f^{A\Rightarrow B\Rightarrow Z}=\text{fmap}\,f\circ\text{ap}
\]
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & F^{B\Rightarrow Z}\ar[rd]\sp(0.45){\text{ap}}\\
F^{A}\ar[ru]\sp(0.45){\text{fmap}\,f}\ar[rr]\sb(0.45){\text{fmap}_{2}\,(f^{A\Rightarrow B\Rightarrow Z})} &  & \left(F^{B}\Rightarrow F^{Z}\right)
}
\]
}{\footnotesize \par}
\item The functions \texttt{\textcolor{blue}{\footnotesize{}fmap$_{3}$}},
\texttt{\textcolor{blue}{\footnotesize{}fmap$_{4}$}} etc.\ can be
defined similarly:{\footnotesize{}
\[
\text{fmap}_{3}\,f^{A\Rightarrow B\Rightarrow C\Rightarrow Z}=\text{fmap}\,f\circ\text{ap}\circ\text{fmap}_{F^{B}\Rightarrow?}\text{ap}
\]
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & F^{B\Rightarrow C\Rightarrow Z}\ar[r]\sp(0.45){\text{ap}^{[B,C\Rightarrow Z]}} & \left(F^{B}\Rightarrow F^{C\Rightarrow Z}\right)\ar[rd]\sp(0.55){\text{fmap}_{F^{B}\Rightarrow?}\text{ap}^{[C,Z]}}\\
F^{A}\ar[ru]\sp(0.45){\text{fmap}\,f}\ar[rrr]\sb(0.45){\text{fmap}_{3}\,(f^{A\Rightarrow B\Rightarrow C\Rightarrow Z})} &  &  & \left(F^{B}\Rightarrow F^{C}\Rightarrow F^{Z}\right)
}
\]
}{\footnotesize \par}
\item Using the infix syntax will get rid of {\footnotesize{}$\text{fmap}_{F^{B}\Rightarrow?}\text{ap}$}
(see example code)
\begin{itemize}
\item Note the pattern: a natural transformation is equivalent to a lifting
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Deriving the \texttt{\textcolor{blue}{\footnotesize{}zip}} operation
from \texttt{\textcolor{blue}{\footnotesize{}map2}} }
\begin{itemize}
\item The types $A\Rightarrow B\Rightarrow C$ and $A\times B\Rightarrow C$
are equivalent (curry/uncurry)
\item Uncurry $\text{fmap}_{2}$ to $\text{fmap2}:\left(A\times B\Rightarrow C\right)\Rightarrow F^{A}\times F^{B}\Rightarrow F^{C}$ 
\item Compute $\text{fmap2}\left(f\right)$ with $f=\text{id}^{A\times B\Rightarrow A\times B}$,
expecting to obtain a simpler natural transformation: 
\[
\text{zip}:F^{A}\times F^{B}\Rightarrow F^{A\times B}
\]
 
\item This is quite similar to \texttt{\textcolor{blue}{\footnotesize{}zip}}
for lists:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}List(1,~2).zip(List(10,~20))~=~List((1,~10),~(2,~20))}~
\end{lyxcode}
\begin{itemize}
\item The functions \texttt{\textcolor{blue}{\footnotesize{}zip}} and \texttt{\textcolor{blue}{\footnotesize{}fmap2}}
are computationally equivalent:{\footnotesize{}
\begin{align*}
\text{zip} & =\text{fmap2}\left(\text{id}\right)\\
\text{fmap2}\,(f^{A\times B\Rightarrow C}) & =\text{zip}\circ\text{fmap}\,f
\end{align*}
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & F^{A\times B}\ar[rd]\sp(0.65){\ \ \text{fmap}\,f^{A\times B\Rightarrow C}}\\
F^{A}\times F^{B}\ar[ru]\sp(0.5){\text{zip}}\ar[rr]\sb(0.6){\text{fmap2}\,(f^{A\times B\Rightarrow C})} &  & F^{C}
}
\]
}{\footnotesize \par}
\item The functor $F$ is \textbf{zippable} if such a \texttt{\textcolor{blue}{\footnotesize{}zip}}
exists (with appropriate laws)
\begin{itemize}
\item The same pattern: a natural transformation is equivalent to a lifting
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{{*} Equivalence of the operations \texttt{\textcolor{blue}{\footnotesize{}ap}}
and \texttt{\textcolor{blue}{\footnotesize{}zip}} }
\begin{itemize}
\item \vspace{-0.2cm}Set $A\equiv B\Rightarrow C$, get $\text{zip}^{[B\Rightarrow C,B]}:F^{B\Rightarrow C}\times F^{B}\Rightarrow F^{(B\Rightarrow C)\times B}$
\item Use \texttt{\textcolor{blue}{\footnotesize{}eval}} $:\left(B\Rightarrow C\right)\times B\Rightarrow C$
and $\text{fmap}\left(\text{eval}\right):F^{(B\Rightarrow C)\times B}\Rightarrow F^{C}$
\item Uncurry: \texttt{\textcolor{blue}{\footnotesize{}app}}$\text{}^{[B,C]}:F^{B\Rightarrow C}\times F^{B}\Rightarrow F^{C}\equiv\text{zip}\circ\text{fmap}\left(\text{eval}\right)$ 
\item The functions \texttt{\textcolor{blue}{\footnotesize{}zip}} and \texttt{\textcolor{blue}{\footnotesize{}app}}
are computationally equivalent:
\begin{itemize}
\item use $\text{pair}:\left(A\Rightarrow B\Rightarrow A\times B\right)=a^{A}\Rightarrow b^{B}\Rightarrow a\times b$
\item use $\text{fmap}\left(\text{pair}\right)\equiv\text{pair}^{\uparrow}$
on an $fa^{F^{A}}$, get $(\text{pair}^{\uparrow}fa):F^{B\Rightarrow A\times B}$;
then{\footnotesize{}
\begin{align*}
\text{zip}\left(fa\times fb\right) & =\text{app}\left((\text{pair}^{\uparrow}fa)\times fb\right)\\
\text{app}^{[B,C]} & =\text{zip}^{[B\Rightarrow C,B]}\circ\text{fmap}\left(\text{eval}\right)
\end{align*}
}
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & F^{(B\Rightarrow C)\times B}\ar[rd]\sp(0.65){\ \ \text{fmap}\left(\text{eval}\right)}\\
F^{B\Rightarrow C}\times F^{B}\ar[ru]\sp(0.5){\text{zip}}\ar[rr]\sb(0.55){\text{app}^{[B,C]}} &  & F^{C}
}
\]
\end{itemize}
\item Rewrite this using curried arguments: $\text{fzip}^{[A,B]}:F^{A}\Rightarrow F^{B}\Rightarrow F^{A\times B}$;
$\text{ap}^{[B,C]}:F^{B\Rightarrow C}\Rightarrow F^{B}\Rightarrow F^{C}$;
then $\text{ap}\,f=\text{fzip}\,f\circ\text{fmap}\left(\text{eval}\right)$. 
\item Now $\text{fzip}\,p^{F^{A}}q^{F^{B}}=\text{ap}\left(\text{pair}^{\uparrow}p\right)q$,
hence we may omit the argument $q$: $\text{fzip}=\text{pair}^{\uparrow}\circ\text{ap}$.
With explicit types: $\text{fzip}^{[A,B]}=\text{pair}^{\uparrow}\circ\text{ap}^{[B,A\Rightarrow B]}$.
\end{itemize}
\end{frame}

\begin{frame}{Motivation for applicative laws. Naturality laws for \texttt{\textcolor{blue}{\footnotesize{}map2}} }

Treat \texttt{\textcolor{blue}{\footnotesize{}map2}} as a replacement
for a monadic block with independent effects:\texttt{\textcolor{blue}{\footnotesize{}\smallskip{}
}}{\footnotesize \par}

\texttt{\textcolor{blue}{\footnotesize{}}}%
\begin{minipage}[c][1\totalheight][t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}for~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~x~$\leftarrow$~cont1}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~y~$\leftarrow$~cont2}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}~yield~g(x,~y)}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}}}%
\begin{minipage}[c][1\totalheight][t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}map2~(}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~cont1,}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~cont2}{\footnotesize \par}

\textcolor{blue}{\footnotesize{})~\{~(x,~y)~$\Rightarrow$~g(x,~y)~\}}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}\medskip{}
}}{\footnotesize \par}
\begin{itemize}
\item Main idea: Formulate the monad laws in terms of \texttt{\textcolor{blue}{\footnotesize{}map2}}
and \texttt{\textcolor{blue}{\footnotesize{}pure}} 
\end{itemize}
Naturality laws: Manipulate data in one of the containers\texttt{\textcolor{blue}{\footnotesize{}\smallskip{}
}}{\footnotesize \par}

\texttt{\textcolor{blue}{\footnotesize{}}}%
\begin{minipage}[c][1\totalheight][t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}for~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~x~$\leftarrow$~cont1.map(f)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~y~$\leftarrow$~cont2}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}~yield~g(x,~y)}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}}}%
\begin{minipage}[c][1\totalheight][t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}for~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~x~$\leftarrow$~cont1}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~y~$\leftarrow$~cont2}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}~yield~g(f(x),~y)}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}\medskip{}
}}{\footnotesize \par}

and similarly for \texttt{\textcolor{blue}{\footnotesize{}cont2}}
instead of \texttt{\textcolor{blue}{\footnotesize{}cont1}}; now rewrite
in terms of for \texttt{\textcolor{blue}{\footnotesize{}map2}}:
\begin{itemize}
\item \textbf{Left naturality} for \texttt{\textcolor{blue}{\footnotesize{}map2}}:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}map2(cont1.map(f),~cont2)(g)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~=~map2(cont1,~cont2)\{~(x,~y)~$\Rightarrow$~g(f(x),~y)~\}}{\footnotesize \par}
\end{lyxcode}
\begin{itemize}
\item \textbf{Right naturality} for \texttt{\textcolor{blue}{\footnotesize{}map2}}:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}map2(cont1,~cont2.map(f))(g)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~=~map2(cont1,~cont2)\{~(x,~y)~$\Rightarrow$~g(x,~f(y))~\}}{\footnotesize \par}
\end{lyxcode}
\end{frame}

\begin{frame}{Associativity and identity laws for \texttt{\textcolor{blue}{\footnotesize{}map2}} }

\vspace{-0.1cm}Inline two generators out of three, in two different
ways:\texttt{\textcolor{blue}{\footnotesize{}\smallskip{}
}}{\footnotesize \par}

\texttt{\textcolor{blue}{\footnotesize{}}}%
\begin{minipage}[c][1\totalheight][t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}for~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~x~$\leftarrow$~cont1}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~(y,~z)~$\leftarrow$~for~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~~~~~~yy~$\leftarrow$~cont2}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~~~~~~zz~$\leftarrow$~cont3}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~~~~\}~yield~(yy,~zz)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}~yield~g(x,~y,~z)}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}}}%
\begin{minipage}[c][1\totalheight][t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}for~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~(x,~y)~$\leftarrow$~for~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~~~~~~~~~~~xx~$\leftarrow$~cont1}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~~~~~~~~~~~yy~$\leftarrow$~cont2}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~~~~~~~~~\}~yield~(xx,~yy)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~z~$\leftarrow$~cont3}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}~yield~g(x,~y,~z)}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}\medskip{}
}}{\footnotesize \par}

Write this in terms of \texttt{\textcolor{blue}{\footnotesize{}map2}}
to obtain the \textbf{associativity law} for \texttt{\textcolor{blue}{\footnotesize{}map2}}:
\begin{lyxcode}
\vspace{-0.1cm}\textcolor{blue}{\footnotesize{}map2(cont1,~map2(cont2,~cont3)((\_,\_))\{~case(x,(y,z))$\Rightarrow$g(x,y,z)\}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~=~map2(map2(cont1,~cont2)((\_,\_)),~cont3)\{~case((x,y),z))$\Rightarrow$g(x,y,z)\}}~
\end{lyxcode}
Empty context precedes a generator, or follows a generator:\texttt{\textcolor{blue}{\footnotesize{}\smallskip{}
}}{\footnotesize \par}

\texttt{\textcolor{blue}{\footnotesize{}}}%
\begin{minipage}[c][1\totalheight][t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}for~\{~x~$\leftarrow$~pure(a)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~~~y~$\leftarrow$~cont}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}~yield~g(x,~y)}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}}}%
\begin{minipage}[c][1\totalheight][t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}for~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~y~$\leftarrow$~cont}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}~yield~g(a,~y)}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}\medskip{}
}}{\footnotesize \par}

Write this in terms of \texttt{\textcolor{blue}{\footnotesize{}map2}}
to obtain the \textbf{identity laws} for \texttt{\textcolor{blue}{\footnotesize{}map2}}
and \texttt{\textcolor{blue}{\footnotesize{}pure}}:
\begin{lyxcode}
\vspace{-0.1cm}\textcolor{blue}{\footnotesize{}map2(pure(a),~cont)(g)~=~cont.map~\{~y~$\Rightarrow$~g(a,~y)~\}}~

\textcolor{blue}{\footnotesize{}map2(cont,~pure(b))(g)~=~cont.map~\{~x~$\Rightarrow$~g(x,~b)~\}}~
\end{lyxcode}
\end{frame}

\begin{frame}{Deriving the laws for \texttt{\textcolor{blue}{\footnotesize{}zip}}:
naturality law}
\begin{itemize}
\item \vspace{-0.2cm}The laws for \texttt{\textcolor{blue}{\footnotesize{}map2}}
in a short notation; here{\footnotesize{} $f\otimes g\equiv\left\{ a\times b\Rightarrow f(a)\times g(b)\right\} $}
{\footnotesize{}
\begin{align*}
\text{fmap2}\left(g^{A\times B\Rightarrow C}\right)\left(f^{\uparrow}q_{1}\times q_{2}\right) & =\text{fmap2}\left(\left(f\otimes\text{id}\right)\circ g\right)\left(q_{1}\times q_{2}\right)\\
\text{fmap2}\left(g^{A\times B\Rightarrow C}\right)\left(q_{1}\times f^{\uparrow}q_{2}\right) & =\text{fmap2}\left(\left(\text{id}\otimes f\right)\circ g\right)\left(q_{1}\times q_{2}\right)\\
\text{fmap2}\left(g_{1.23}\right)\left(q_{1}\times\text{fmap2}\left(\text{id}\right)\left(q_{2}\times q_{3}\right)\right) & =\text{fmap2}\left(g_{12.3}\right)\left(\text{fmap2}\left(\text{id}\right)\left(q_{1}\times q_{2}\right)\times q_{3}\right)\\
\text{fmap2}\left(g^{A\times B\Rightarrow C}\right)\left(\text{pure}\,a^{A}\times q_{2}^{F^{B}}\right) & =\left(b\Rightarrow g\left(a\times b\right)\right)^{\uparrow}q_{2}\\
\text{fmap2}\left(g^{A\times B\Rightarrow C}\right)\left(q_{1}^{F^{A}}\times\text{pure}\,b^{B}\right) & =\left(a\Rightarrow g\left(a\times b\right)\right)^{\uparrow}q_{1}
\end{align*}
}{\footnotesize \par}
\item Express \texttt{\textcolor{blue}{\footnotesize{}map2}} through \texttt{\textcolor{blue}{\footnotesize{}zip}}:{\footnotesize{}
\begin{align*}
\text{fmap}_{2}\,g^{A\times B\Rightarrow C}\left(q_{1}^{F^{A}}\times q_{2}^{F^{B}}\right) & \equiv\left(\text{zip}\circ g^{\uparrow}\right)\left(q_{1}\times q_{2}\right)\\
\text{fmap}_{2}\,g^{A\times B\Rightarrow C} & \equiv\text{zip}\circ g^{\uparrow}
\end{align*}
}{\footnotesize \par}
\item Combine the two naturality laws into one by using two functions $f_{1}$,
$f_{2}$:{\footnotesize{}
\begin{align*}
\left(f_{1}^{\uparrow}\otimes f_{2}^{\uparrow}\right)\circ\text{fmap2}\,g & =\text{fmap2}\left(\left(f_{1}\otimes f_{2}\right)^{\uparrow}\circ g\right)\\
\left(f_{1}^{\uparrow}\otimes f_{2}^{\uparrow}\right)\circ\text{zip}\circ g^{\uparrow} & =\text{zip}\circ\left(f_{1}\otimes f_{2}\right)^{\uparrow}\circ g^{\uparrow}
\end{align*}
}{\footnotesize \par}
\item \vspace{-0.2cm}The \textbf{naturality law} for \texttt{\textcolor{blue}{\footnotesize{}zip}}
then becomes: {\footnotesize{}$\left(f_{1}^{\uparrow}\otimes f_{2}^{\uparrow}\right)\circ\text{zip}=\text{zip}\circ\left(f_{1}\otimes f_{2}\right)^{\uparrow}$} 
\end{itemize}
\end{frame}

\begin{frame}{Deriving the laws for \texttt{\textcolor{blue}{\footnotesize{}zip}}:
associativity law}
\begin{itemize}
\item Express \texttt{\textcolor{blue}{\footnotesize{}map2}} through \texttt{\textcolor{blue}{\footnotesize{}zip}}
and substitute into the associativity law:{\footnotesize{}
\[
g_{1.23}^{\uparrow}\left(\text{zip}\left(q_{1}\times\text{zip}\left(q_{2}\times q_{3}\right)\right)\right)=g_{12.3}^{\uparrow}\left(\text{zip}\left(\text{zip}\left(q_{1}\times q_{2}\right)\times q_{3}\right)\right)
\]
}{\footnotesize \par}
\item The arbitrary function $g$ is preceded by transformations of the
tuples,{\footnotesize{}
\[
a\times\left(b\times c\right)\equiv\left(a\times b\right)\times c\quad\text{(type isomorphism)}
\]
}{\footnotesize \par}
\item Assume that the isomorphism transformations are applied as needed,
then we may formulate the \textbf{associativity law} for \texttt{\textcolor{blue}{\footnotesize{}zip}}
more concisely:{\footnotesize{}
\[
\text{zip}\left(\text{zip}\left(q_{1}\times q_{2}\right)\times q_{3}\right)\cong\text{zip}\left(q_{1}\times\text{zip}\left(q_{2}\times q_{3}\right)\right)
\]
}\vspace{-0.2cm}
\[
\xymatrix{\xyScaleY{1.4pc}\xyScaleX{3pc}F^{\left(A\times B\right)\times C}\ar[r] & F^{A\times B\times C}\ar[r]\ar[l] & F^{A\times\left(B\times C\right)}\ar[l]\\
F^{A\times B}\times F^{C}\ar[u]\sp(0.6){\text{zip}} & F^{A}\ar[ldd]\ar[r] & F^{A}\times F^{B\times C}\ar[u]\sb(0.6){\text{zip}}\\
F^{A\times B}\ar[u] & F^{C}\ar[rd]\ar[lu] & F^{B\times C}\ar[u]\\
F^{A}\times F^{B}\ar[u]\sp(0.6){\text{zip}} & F^{B}\ar[r]\ar[l] & F^{B}\times F^{C}\ar[u]\sb(0.6){\text{zip}}
}
\]
\end{itemize}
\end{frame}

\begin{frame}{Deriving the laws for \texttt{\textcolor{blue}{\footnotesize{}zip}}:
identity laws}
\begin{itemize}
\item \vspace{-0.2cm}Identity laws seem to be complicated, e.g.\ the left
identity:{\footnotesize{}
\[
g^{\uparrow}\left(\text{zip}\left(\text{pure}\,a\times q\right)\right)=\left(b\Rightarrow g\left(a\times b\right)\right)^{\uparrow}q
\]
}{\footnotesize \par}
\item Replace \texttt{\textcolor{blue}{\footnotesize{}pure}} by an \emph{equivalent}
``wrapped unit'' method \texttt{\textcolor{blue}{\footnotesize{}wu:\ F{[}Unit{]}}}{\footnotesize{}
\[
\text{wu}^{F^{1}}\equiv\text{pure}\left(1\right);\quad\text{pure}(a^{A})=\left(1\Rightarrow a\right)^{\uparrow}\text{wu}
\]
}Then the left identity law can be simplified using left naturality:{\footnotesize{}
\[
g^{\uparrow}\left(\text{zip}\left((\left(1\Rightarrow a\right)^{\uparrow}\text{wu})\times q\right)\right)=g^{\uparrow}\left(\left((1\Rightarrow a)\otimes\text{id}\right)^{\uparrow}\text{zip}\left(\text{wu}\times q\right)\right)
\]
}{\footnotesize \par}
\item Denote {\footnotesize{}$\phi^{B\Rightarrow1\times B}\equiv b\Rightarrow1\times b$}
and {\footnotesize{}$\beta_{a}^{1\times B\Rightarrow A\times B}\equiv\left(1\Rightarrow a\right)\otimes\text{id}$};
then the function {\footnotesize{}$b\Rightarrow g\left(a\times b\right)$}
can be expressed more simply as {\footnotesize{}$\phi\circ\beta_{a}\circ g$},
and the identity law becomes{\footnotesize{}
\[
g^{\uparrow}(\beta_{a}^{\uparrow}\,\text{zip}\left(\text{wu}\times q\right))=\left(\beta_{a}\circ g\right)^{\uparrow}\left(\text{zip}\left(\text{wu}\times q\right)\right)=\left(\phi\circ\beta_{a}\circ g\right)^{\uparrow}q=\left(\beta_{a}\circ g\right)^{\uparrow}(\phi^{\uparrow}q)
\]
}Omitting the common prefix {\footnotesize{}$\left(\beta_{a}\circ g\right)^{\uparrow}$},
we obtain the \textbf{left identity} law:{\footnotesize{}
\[
\text{zip}\left(\text{wu}\times q\right)=\phi^{\uparrow}q
\]
}{\footnotesize \par}
\begin{itemize}
\item Note that $\phi^{\uparrow}$ is an isomorphism between $F^{B}$ and
$F^{1\times B}$
\begin{itemize}
\item Assume that this isomorphism is applied as needed, then we may write{\footnotesize{}
\[
\text{zip}\left(\text{wu}\times q\right)\cong q
\]
}{\footnotesize \par}
\end{itemize}
\item Similarly, the \textbf{right identity} law can be written as {\footnotesize{}$\text{zip}\left(q\times\text{wu}\right)\cong q$}{\footnotesize \par}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Similarity between applicative laws and monoid laws}
\begin{itemize}
\item Define infix syntax for \texttt{\textcolor{blue}{\footnotesize{}zip}}
and write $\text{zip}\left(p\times q\right)\equiv p\bowtie q$
\item Then the associativity and identity laws may be written as{\footnotesize{}
\begin{align*}
q_{1}\bowtie\left(q_{2}\bowtie q_{3}\right) & \cong\left(q_{1}\bowtie q_{2}\right)\bowtie q_{3}\\
\left(\text{wu}\,\bowtie q\right) & \cong q\\
\left(q\bowtie\text{wu}\right) & \cong q
\end{align*}
}These are the laws of a monoid (with some assumed transformations)
\item Naturality law for \texttt{\textcolor{blue}{\footnotesize{}zip}} written
in the infix syntax:{\footnotesize{}
\[
f_{1}^{\uparrow}q_{1}\bowtie f_{2}^{\uparrow}q_{2}=\left(f_{1}\otimes f_{2}\right)^{\uparrow}\left(q_{1}\bowtie q_{2}\right)
\]
}{\footnotesize \par}
\item \texttt{\textcolor{blue}{\footnotesize{}wu}} has no laws; the naturality
for \texttt{\textcolor{blue}{\footnotesize{}pure}} follows automatically
\item The laws are simplest when formulated in terms of \texttt{\textcolor{blue}{\footnotesize{}zip}}
and \texttt{\textcolor{blue}{\footnotesize{}wu}} 
\begin{itemize}
\item Naturality for \texttt{\textcolor{blue}{\footnotesize{}zip}} will
usually follow from parametricity
\begin{itemize}
\item A third naturality law for \texttt{\textcolor{blue}{\footnotesize{}map2}}
follows from defining \texttt{\textcolor{blue}{\footnotesize{}map2}}
through \texttt{\textcolor{blue}{\footnotesize{}zip}}!
\end{itemize}
\end{itemize}
\item ``Zippable'' functors have only the associativity and naturality
laws
\item Applicative functors are a strict superset of monadic functors
\begin{itemize}
\item There are applicative functors that \emph{cannot} be monads
\item Applicative functor implementation may disagree with the monad
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{A third naturality law for \texttt{\textcolor{blue}{\footnotesize{}map2}} }
\begin{itemize}
\item \vspace{-0.1cm}There must be one more naturality law for \texttt{\textcolor{blue}{\footnotesize{}map2}} 
\item Transform the result of a \texttt{\textcolor{blue}{\footnotesize{}map2}}:\texttt{\textcolor{blue}{\footnotesize{}\smallskip{}
}}{\footnotesize \par}
\end{itemize}
\texttt{\textcolor{blue}{\footnotesize{}}}%
\begin{minipage}[c][1\totalheight][t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}(~for~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~x~$\leftarrow$~cont1}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~y~$\leftarrow$~cont2}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}~yield~g(x,~y)~~).map(f)}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}}}%
\begin{minipage}[c][1\totalheight][t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}for~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~x~$\leftarrow$~cont1}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~y~$\leftarrow$~cont2}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}~yield~f(~g(x,~y)~)}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}\hfill{}\medskip{}
}}{\footnotesize \par}
\begin{itemize}
\item Write this in terms of \texttt{\textcolor{blue}{\footnotesize{}map2}},
obtain a third naturality law:
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}map2(cont1,~cont2)(g).map(f)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~=~map2(cont1,~cont2)(g~andThen~f)}{\footnotesize{}
\begin{align*}
\text{fmap}2\left(g\right)\circ f^{\uparrow} & =\text{fmap2}\left(g\circ f\right)\\
f^{\uparrow}\left(\text{fmap}2\left(g\right)\left(p\times q\right)\right) & =\text{fmap2}\left(g\circ f\right)\left(p\times q\right)
\end{align*}
}{\footnotesize \par}
\end{lyxcode}
\begin{itemize}
\item This law automatically follows if we define \texttt{\textcolor{blue}{\footnotesize{}map2}}
through \texttt{\textcolor{blue}{\footnotesize{}zip}}:{\footnotesize{}
\[
\text{fmap}2\left(g\right)\circ f^{\uparrow}=\text{zip}\circ g^{\uparrow}\circ f^{\uparrow}=\text{zip}\circ\left(g\circ f\right)^{\uparrow}
\]
}{\footnotesize \par}
\item Note: We always have one naturality law per type parameter
\end{itemize}
\end{frame}

\begin{frame}{Applicative operation \texttt{\textcolor{blue}{\footnotesize{}ap}}
as a ``lifting''}
\begin{itemize}
\item \vspace{-0.18cm}Consider \texttt{\textcolor{blue}{\footnotesize{}ap}}
as a ``lifting'' since it has type{\footnotesize{} $F^{A\Rightarrow B}\Rightarrow\left(F^{A}\Rightarrow F^{B}\right)$}{\footnotesize \par}
\item A ``lifting'' should obey the identity and the composition laws
\begin{itemize}
\item An ``identity'' value of type $F^{A\Rightarrow A}$, mapped to $\text{id}^{F^{A}\Rightarrow F^{A}}$
by \texttt{\textcolor{blue}{\footnotesize{}ap}} 
\begin{itemize}
\item A good candidate for that value is $\text{id}_{\odot}\equiv\text{pure}\left(\text{id}^{A\Rightarrow A}\right)$
\end{itemize}
\item A ``composition'' of an $F^{A\Rightarrow B}$ and an $F^{B\Rightarrow C}$,
yielding an $F^{A\Rightarrow C}$
\begin{itemize}
\item We can use \texttt{\textcolor{blue}{\footnotesize{}map2}} to implement
this composition, denoted $g\odot h$:
\[
g^{F^{A\Rightarrow B}}\odot h^{F^{B\Rightarrow C}}\equiv\text{fmap2}\,(p^{A\Rightarrow B}\times q^{B\Rightarrow C}\Rightarrow p\circ q)\left(g,h\right)
\]
\end{itemize}
\end{itemize}
\item What are the laws that follow for $g\odot h$ from the \texttt{\textcolor{blue}{\footnotesize{}map2}}
laws?{\footnotesize{}
\begin{align*}
\text{id}_{\odot}\odot h=h; & \quad g\odot\text{id}_{\odot}=g\\
g^{F^{A\Rightarrow B}}\odot(h^{F^{B\Rightarrow C}}\odot k^{F^{C\Rightarrow D}}) & =\left(g\odot h\right)\odot k\\
\left((x^{B\Rightarrow C}\Rightarrow f^{A\Rightarrow B}\circ x)^{\uparrow}g^{F^{B\Rightarrow C}}\right)\odot h^{F^{C\Rightarrow D}} & =(x^{B\Rightarrow D}\Rightarrow f^{A\Rightarrow B}\circ x)^{\uparrow}\left(g\odot h\right)\\
g^{F^{A\Rightarrow B}}\odot\left((x^{B\Rightarrow C}\Rightarrow x\circ f^{C\Rightarrow D})^{\uparrow}h^{F^{B\Rightarrow C}}\right) & =(x^{A\Rightarrow C}\Rightarrow x\circ f^{C\Rightarrow D})^{\uparrow}\left(g\odot h\right)
\end{align*}
}{\footnotesize \par}
\begin{itemize}
\item The first 3 laws are the identity \& associativity laws of a \emph{category}
\begin{itemize}
\item The morphism type is $A\rightsquigarrow B\equiv F^{A\Rightarrow B}$,
the composition is $\odot$
\end{itemize}
\item The last 2 laws are naturality laws, connecting $\text{fmap}$ and
$\odot$
\end{itemize}
\item Therefore \texttt{\textcolor{blue}{\footnotesize{}ap}} is a functor's
``lifting'' of morphisms from two categories
\end{itemize}
\end{frame}

\begin{frame}{Deriving the category laws for $\left(\text{id}_{\odot},\odot\right)$}

\vspace{-0.10cm}The five laws for $\text{id}_{\odot}$ and $\odot$
follow from the five \texttt{\textcolor{blue}{\footnotesize{}map2}}
laws
\begin{itemize}
\item Consider $\text{id}_{\odot}\odot h$ and substitute the definition
of $\odot$ via \texttt{\textcolor{blue}{\footnotesize{}map2}}, cf.\ slide
7: $\text{id}_{\odot}\odot h=\text{fmap2}\left(p\times q\Rightarrow p\circ q\right)\left(\text{pure}\left(\text{id}\right)\times h\right)=\left(b\Rightarrow\text{id}\circ b\right)^{\uparrow}h=h$
\item The law $g\odot\text{id}_{\odot}=g$ is derived similarly
\item Associativity law: {\footnotesize{}$g\odot\left(h\odot k\right)=\text{fmap2}\left(\circ\right)\left(g\times\text{fmap2}\left(\circ\right)\left(h\times k\right)\right)$}
The 3rd naturality law gives:{\footnotesize{} $\text{fmap2}\left(\circ\right)\left(h\times k\right)=\left(\circ\right)^{\uparrow}\left(\text{fmap2}\left(\text{id}\right)\left(h\times k\right)\right)$},
and then:{\footnotesize{}
\begin{align*}
g\odot\left(h\odot k\right) & =\text{fmap2}\left(x\times\left(y\times z\right)\Rightarrow x\circ y\circ z\right)\left(g\times\text{fmap2}\left(\text{id}\right)\left(h\times k\right)\right)\\
\left(g\odot h\right)\odot k & =\text{fmap2}\left(\left(x\times y\right)\times z\Rightarrow x\circ y\circ z\right)\left(\text{fmap2}\left(\text{id}\right)\left(g\times h\right)\times k\right)
\end{align*}
}Now the associativity law for{\footnotesize{} $\text{fmap2}$ }yields
{\footnotesize{}$g\odot\left(h\odot k\right)=\left(g\odot h\right)\odot k$}{\footnotesize \par}
\item Derive naturality laws for $\odot$ from the three {\footnotesize{}$\text{map}_{2}$}
naturality laws: {\footnotesize{}$\left((x\Rightarrow f\circ x)^{\uparrow}g\right)\odot h=\text{fmap2}\left(\circ\right)\left((x\Rightarrow f\circ x)^{\uparrow}g\times h\right)=$
$\text{fmap2}\left(x\times y\Rightarrow f\circ x\circ y\right)\left(g\times h\right)=\left(x\Rightarrow f\circ x\right)^{\uparrow}\left(\text{fmap2}\left(\circ\right)\left(g\times h\right)\right)=\left(x\Rightarrow f\circ x\right)^{\uparrow}\left(g\odot h\right)$}{\footnotesize \par}
\item The law is {\footnotesize{}$g\odot(x\Rightarrow x\circ f)^{\uparrow}h=(x\Rightarrow x\circ f)^{\uparrow}\left(g\odot h\right)$}
is derived similarly
\end{itemize}
\end{frame}

\begin{frame}{Deriving the functor laws for \texttt{\textcolor{blue}{\footnotesize{}ap}} }

\vspace{-0.10cm}Now that we established the laws for $\odot$, we
have \texttt{\textcolor{blue}{\footnotesize{}ap}} laws:
\[
\text{ap}^{[B,Z]}:F^{B\Rightarrow Z}\Rightarrow F^{B}\Rightarrow F^{Z}=\text{fmap}_{2}\left(\text{id}^{\left(B\Rightarrow Z\right)\Rightarrow\left(B\Rightarrow Z\right)}\right)
\]

Identity law: $\text{ap}\left(\text{id}_{\odot}\right)=\text{id}^{F^{A}\Rightarrow F^{A}}$
\begin{itemize}
\item Derivation:{\footnotesize{} $\text{ap}\,(\text{id}_{\odot}^{F^{A\Rightarrow A}})\,(q^{F^{A}})=\text{fmap}_{2}(\text{id}^{\left(A\Rightarrow A\right)\Rightarrow A\Rightarrow A})\,(\text{pure}\,(\text{id}^{A\Rightarrow A}))\,(q^{F^{A}})=$}
{\footnotesize{}$\text{fmap2}\left(f\times x\Rightarrow f(x)\right)\left(\text{pure}\left(\text{id}\right)\times q\right)=$
$\left(x\Rightarrow\text{id}(x)\right)^{\uparrow}q=\text{id}^{\uparrow}q=q$} 
\item Easier derivation: first, express {\footnotesize{}$\text{ap}$} via
$\odot$ using the isomorphisms{\footnotesize{}
\[
A\cong1\Rightarrow A;\quad F^{A}\cong F^{1\Rightarrow A}
\]
}Then {\footnotesize{}$\text{ap}\,(p^{F^{B\Rightarrow Z}})\,(q^{F^{B}})\cong q^{F^{1\Rightarrow B}}\odot p^{F^{B\Rightarrow Z}}$}
and so {\footnotesize{}$\text{ap}\left(\text{id}_{\odot}\right)\left(q\right)\cong q\odot\text{id}_{\odot}=q$}{\footnotesize \par}
\end{itemize}
Composition law: $\text{ap}\left(g\odot h\right)=\text{ap}\left(g\right)\circ\text{ap}\left(h\right)$
\begin{itemize}
\item Derivation: use $\text{ap}\,p\,q\cong q\odot p$ to get {\footnotesize{}$\text{ap}\left(g\odot h\right)\left(q\right)\cong q\odot\left(g\odot h\right)$}
while {\footnotesize{}$\left(\text{ap}\left(g\right)\circ\text{ap}\left(h\right)\right)q=$
$\text{ap}\left(h\right)\left(\text{ap}\left(g\right)\left(q\right)\right)\cong\text{ap}\left(h\right)\left(q\odot g\right)\cong\left(q\odot g\right)\odot h$}{\footnotesize \par}
\end{itemize}
\end{frame}

\begin{frame}{Constructions of applicative functors}
\begin{itemize}
\item \vspace{-0.10cm}All monadic constructions still hold for applicative
functors
\item Additionally, there are some non-monadic constructions
\end{itemize}
\begin{enumerate}
\item $F^{A}\equiv1$ (constant functor) and $F^{A}\equiv A$ (identity
functor)
\item $F^{A}\equiv G^{A}\times H^{A}$ for any applicative $G^{A}$ and
$H^{A}$
\begin{itemize}
\item but $G^{A}+H^{A}$ is in general \emph{not} applicative
\end{itemize}
\item $F^{A}\equiv A+G^{A}$ for any applicative $G^{A}$ (\textbf{free
pointed} over $G$)
\item $F^{A}\equiv A+G^{F^{A}}$ (recursive) for \emph{any} functor $G^{A}$
(\textbf{free monad} over $G$)
\item $F^{A}\equiv H^{A}\Rightarrow A$ for \emph{any} contrafunctor $H^{A}$\\
Constructions that do not correspond to monadic ones:
\item $F^{A}\equiv Z$ (constant functor, $Z$ a monoid)
\item $F^{A}\equiv Z+G^{A}$ for any applicative $G^{A}$ and monoid $Z$
\item $F^{A}\equiv G^{H^{A}}$ when both $G$ and $H$ are applicative
\end{enumerate}
\begin{itemize}
\item Applicative that disagrees with its monad: $F^{A}\equiv1+\left(1\Rightarrow A\times F^{A}\right)$ 
\item Examples of non-applicative functors: $F^{A}\equiv\left(P\Rightarrow A\right)+\left(Q\Rightarrow A\right)$,
$F^{A}\equiv\left(A\Rightarrow P\right)\Rightarrow Q$,\  $F^{A}\equiv\left(A\Rightarrow P\right)\Rightarrow1+A$
\end{itemize}
\end{frame}

\begin{frame}{All non-parameterized exp-poly types are monoids}
\begin{itemize}
\item \vspace{-0.1cm}Using known monoid constructions (Chapter\ 7), we
can implement $X+Y$, $X\times Y$, $X\Rightarrow Y$ as monoids when
$X$ and $Y$ are monoids
\item All primitive types have at least one monoid instance:
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}Int}}, \texttt{\textcolor{blue}{\footnotesize{}Float}},
\texttt{\textcolor{blue}{\footnotesize{}Double}}, \texttt{\textcolor{blue}{\footnotesize{}Char}},
\texttt{\textcolor{blue}{\footnotesize{}Boolean}} are ``numeric''
monoids
\item \texttt{\textcolor{blue}{\footnotesize{}Seq{[}A{]}}}, \texttt{\textcolor{blue}{\footnotesize{}Set{[}A{]}}},
\texttt{\textcolor{blue}{\footnotesize{}Map{[}K,V{]}}} are set-like
monoids
\item \texttt{\textcolor{blue}{\footnotesize{}String}} is equivalent to
a sequence of integers; \texttt{\textcolor{blue}{\footnotesize{}Unit}}
is a trivial monoid
\end{itemize}
\item Therefore, all exponential-polynomial types without type parameters
are monoids in at least one way
\item Example of an exponential-polynomial type without type parameters:
{\footnotesize{}$\text{Int}+\text{String}\times\text{String}\times\left(\text{Int}\Rightarrow\text{Bool}\right)+\left(\text{Bool}\times\text{String}\Rightarrow1+\text{String}\right)$} 
\item Example of a non-monoid type with type parameters: $A\Rightarrow B$
\end{itemize}
By constructions 1, 2, 6, 7, \emph{all} polynomial $F^{A}$ with monoidal
coefficients are applicative: write $F^{A}=Z_{1}+A\times\left(Z_{2}+A\times...\right)$
with some monoids $Z_{i}$
\begin{itemize}
\item Examples: $F^{A}=1+A\times A$ (this $F^{A}$ cannot be a monad!)
\item $F^{A}=A+A\times A\times Z$ where $Z$ is a monoid (this $F^{A}$
is a monad)
\end{itemize}
Previous examples of non-applicative functors are all \emph{non-polynomial}
\end{frame}

\begin{frame}{Definition and constructions of applicative contrafunctors}
\begin{itemize}
\item \vspace{-0.25cm}The applicative functor laws, if formulated via \texttt{\textcolor{blue}{\footnotesize{}zip}}
and \texttt{\textcolor{blue}{\footnotesize{}wu}}, do not use \texttt{\textcolor{blue}{\footnotesize{}map}}
and therefore can be formulated for contrafunctors
\item Define an \textbf{applicative contrafunctor} $C^{A}$ as having \texttt{\textcolor{blue}{\footnotesize{}zip}}
and \texttt{\textcolor{blue}{\footnotesize{}wu}}:{\footnotesize{}tnotesize{}wu}}:{\footnotesize{}
\[
\text{zip}:C^{A}\times C^{B}\Rightarrow C^{A\times B};\quad\text{wu}:C^{1}
\]
}{\footnotesize \par}
\item Identity and associativity laws must hold for \texttt{\textcolor{blue}{\footnotesize{}zip}}
and \texttt{\textcolor{blue}{\footnotesize{}wu}} 
\begin{itemize}
\item Note: applying \texttt{\textcolor{blue}{\footnotesize{}contramap}}
to the function $a\times b\Rightarrow a$ will yield some $C^{A}\Rightarrow C^{A\times B}$,
but this will \emph{not} give a valid implementation of \texttt{\textcolor{blue}{\footnotesize{}zip}}!
\end{itemize}
\item Naturality must hold for \texttt{\textcolor{blue}{\footnotesize{}zip}},
but with \texttt{\textcolor{blue}{\footnotesize{}contramap}} instead
of \texttt{\textcolor{blue}{\footnotesize{}map}} 
\begin{itemize}
\item There are no corresponding \texttt{\textcolor{blue}{\footnotesize{}pure}}
or \texttt{\textcolor{blue}{\footnotesize{}contraap}}! But have $\forall A:C^{A}$
\end{itemize}
\end{itemize}
Applicative contrafunctor constructions:
\begin{enumerate}
\item $C^{A}\equiv Z$ (constant functor, $Z$ a monoid)
\item $C^{A}\equiv G^{A}\times H^{A}$ for any applicative contrafunctors
$G^{A}$ and $H^{A}$
\item $C^{A}\equiv G^{A}+H^{A}$ for any applicative contrafunctors $G^{A}$
and $H^{A}$
\item $C^{A}\equiv H^{A}\Rightarrow G^{A}$ for \emph{any} \emph{functor}
$H^{A}$ and applicative contrafunctor $G^{A}$
\item $C^{A}\equiv G^{H^{A}}$ if a functor $G^{A}$ and contrafunctor $H^{A}$
are both applicative
\end{enumerate}
\begin{itemize}
\item \emph{All} exponential-polynomial contrafunctors with monoidal coefficients
are applicative! (These constructions cover all exp-poly cases.)
\end{itemize}
\end{frame}

\begin{frame}{Definition and laws of profunctors}
\begin{itemize}
\item \textbf{Profunctors} have the type parameter in both contravariant
and covariant positions; they can have neither \texttt{\textcolor{blue}{\footnotesize{}map}}
nor \texttt{\textcolor{blue}{\footnotesize{}contramap}} 
\item Examples of profunctors: {\footnotesize{}$P^{A}\equiv1+\text{Int}\times A\Rightarrow A$;
$P^{A}\equiv A+\left(A\Rightarrow\text{String}\right)$}{\footnotesize \par}
\item Example of non-profunctor: a GADT, {\footnotesize{}$F^{A}\equiv\text{String}^{F^{\text{Int}}}+\text{Int}^{F^{1}}$}{\footnotesize \par}
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}sealed~trait~F{[}A{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}final~case~class~F1(s:~String)~extends~F{[}Int{]}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}final~case~class~F2(i:~Int)~extends~F{[}Unit{]}}{\footnotesize \par}
\end{lyxcode}
\begin{itemize}
\item Rigorously: $P^{A}$ is a profunctor if a type function $Q^{X,Y}$
exists which is a contrafunctor in $X$ and a functor in $Y$, and
such that $P^{A}\equiv Q^{A,A}$
\item Profunctors have \texttt{\textcolor{blue}{\footnotesize{}xmap}} of
type {\footnotesize{}$\left(A\Rightarrow B\right)\times\left(B\Rightarrow A\right)\Rightarrow(P^{A}\Rightarrow P^{B})$ }{\footnotesize \par}
\item Identity law: {\footnotesize{}$\text{xmap}\left(\text{id},\text{id}\right)=\text{id}$}{\footnotesize \par}
\item Composition law: {\footnotesize{}$\text{xmap}\left(f_{1},g_{1}\right)\circ\text{xmap}\left(f_{2},g_{2}\right)=\text{xmap}\left(f_{1}\circ f_{2},g_{2}\circ g_{1}\right)$}{\footnotesize \par}
\begin{itemize}
\item both \texttt{\textcolor{blue}{\footnotesize{}xmap}} and the laws follow
from the functor and contrafunctor laws
\end{itemize}
\item \emph{All} exp-poly type constructors are profunctors since the type
parameter is always in either a covariant or a contravariant position
\end{itemize}
\end{frame}

\begin{frame}{Definition and constructions of applicative profunctors}
\begin{itemize}
\item Definition of \textbf{applicative profunctor}: has \texttt{\textcolor{blue}{\footnotesize{}zip}}
and \texttt{\textcolor{blue}{\footnotesize{}wu}} with the laws
\begin{itemize}
\item There is no corresponding \texttt{\textcolor{blue}{\footnotesize{}ap}}!
But have \texttt{\textcolor{blue}{\footnotesize{}pure}} {\footnotesize{}$:A\Rightarrow P^{A}$} 
\end{itemize}
\end{itemize}
Applicative profunctors admit all previous constructions, and in addition:
\begin{enumerate}
\item $P^{A}\equiv G^{A}\times H^{A}$ for any applicative profunctors $G^{A}$
and $H^{A}$
\item $P^{A}\equiv Z+G^{A}$ for any applicative profunctor $G^{A}$ and
monoid $Z$
\item $P^{A}\equiv A+G^{A}$ for any applicative profunctor $G^{A}$
\item $P^{A}\equiv F^{A}\Rightarrow Q^{A}$ for \emph{any} \emph{functor}
$F^{A}$ and applicative profunctor $Q^{A}$
\begin{itemize}
\item Non-working construction: $P^{A}\equiv H^{A}\Rightarrow A$ for a
profunctor $H^{A}$
\end{itemize}
\item $P^{A}\equiv G^{H^{A}}$ for a functor $G^{A}$ and a profunctor $H^{A}$,
both applicative
\end{enumerate}
\end{frame}

\begin{frame}{Commutative applicative functors}
\begin{itemize}
\item \vspace{-0.15cm}The monoidal operation $\oplus$ can be \textbf{commutative}
w.r.t.\ its arguments:{\footnotesize{}
\[
x\oplus y=y\oplus x
\]
}{\footnotesize \par}
\item Applicative operation \texttt{\textcolor{blue}{\footnotesize{}zip}}
can be \textbf{commutative} w.r.t.\ its arguments:{\footnotesize{}
\[
\left(a\times b\Rightarrow b\times a\right)^{\uparrow}\left(fa\bowtie fb\right)=fb\bowtie fa
\]
}or $fa\bowtie fb\cong fb\bowtie fa$, implicitly using the isomorphism
$a\times b\Rightarrow b\times a$
\item Applicative functor is commutative if the second effect is independent
of the first effect (not only of the first value)
\item Examples:
\begin{itemize}
\item $\text{List}$ is commutative; applicative parsers are not
\item If defined through the monad instance, \texttt{\textcolor{blue}{\footnotesize{}zip}}
is usually not commutative
\item All polynomial functors with \emph{commutative} monoidal coefficients
are commutative applicative functors 
\end{itemize}
\item Most applicative constructions preserve commutativity 
\item The same applies to applicative contrafunctors and profunctors 
\item Commutativity makes proving associativity easier: {\footnotesize{}
\[
\left(fa\bowtie fb\right)\bowtie fc\cong fc\bowtie\left(fb\bowtie fa\right)
\]
}so it's sufficient to swap $fa$ and $fc$ and show equivalence
\end{itemize}
\end{frame}

\begin{frame}{Categorical overview of ``regular'' functor classes}

\vspace{-0.15cm}The ``liftings'' show the types of category's morphisms
\begin{center}
\vspace{-0.08cm}%
\begin{tabular}{|c|c|c|}
\hline 
\textbf{\scriptsize{}class name} & \textbf{\scriptsize{}lifting's name and type signature} & \textbf{\scriptsize{}category's morphism}\tabularnewline
\hline 
\hline 
{\scriptsize{}functor} & {\scriptsize{}$\text{fmap}:\left(A\Rightarrow B\right)\Rightarrow F^{A}\Rightarrow F^{B}$} & {\scriptsize{}$A\Rightarrow B$}\tabularnewline
\hline 
{\scriptsize{}filterable} & {\scriptsize{}$\text{fmapOpt}:\left(A\Rightarrow1+B\right)\Rightarrow F^{A}\Rightarrow F^{B}$} & {\scriptsize{}$A\Rightarrow1+B$}\tabularnewline
\hline 
{\scriptsize{}monad} & {\scriptsize{}$\text{flm}:\left(A\Rightarrow F^{B}\right)\Rightarrow F^{A}\Rightarrow F^{B}$} & {\scriptsize{}$A\Rightarrow F^{B}$}\tabularnewline
\hline 
{\scriptsize{}applicative} & {\scriptsize{}$\text{ap}:F^{A\Rightarrow B}\Rightarrow F^{A}\Rightarrow F^{B}$} & {\scriptsize{}$F^{A\Rightarrow B}$}\tabularnewline
\hline 
{\scriptsize{}contrafunctor} & {\scriptsize{}$\text{contrafmap}:\left(B\Rightarrow A\right)\Rightarrow F^{A}\Rightarrow F^{B}$} & {\scriptsize{}$B\Rightarrow A$}\tabularnewline
\hline 
{\scriptsize{}profunctor} & {\scriptsize{}$\text{xmap}:\left(A\Rightarrow B\right)\times\left(B\Rightarrow A\right)\Rightarrow F^{A}\Rightarrow F^{B}$} & {\scriptsize{}$\left(A\Rightarrow B\right)\times\left(B\Rightarrow A\right)$}\tabularnewline
\hline 
{\scriptsize{}contra-filterable} & {\scriptsize{}$\text{contrafmapOpt}:\left(B\Rightarrow1+A\right)\Rightarrow F^{A}\Rightarrow F^{B}$} & {\scriptsize{}$B\Rightarrow1+A$}\tabularnewline
\hline 
\multicolumn{1}{|c}{} & \multicolumn{1}{c}{{\scriptsize{}Not yet considered:}} & \tabularnewline
\hline 
{\scriptsize{}comonad} & {\scriptsize{}$\text{coflm}:\left(F^{A}\Rightarrow B\right)\Rightarrow F^{A}\Rightarrow F^{B}$} & {\scriptsize{}$F^{A}\Rightarrow B$}\tabularnewline
\hline 
\end{tabular}
\par\end{center}

Need to define each category's composition and identity morphism

Then impose the category laws, the naturality laws, and the functor
laws
\begin{itemize}
\item Obtained a systematic picture of the ``regular'' type classes
\item Some classes (e.g.\ contra-applicative) aren't covered by this scheme
\item Some of the possibilities (e.g.\ ``contramonad'') don't actually
work out
\end{itemize}
\end{frame}

\begin{frame}{Exercises}
\begin{enumerate}
\item {\footnotesize{}\vspace{-0.15cm}Show that }\texttt{\textcolor{blue}{\footnotesize{}pure}}{\footnotesize{}
will be automatically a natural transformation when it is defined
using }\texttt{\textcolor{blue}{\footnotesize{}wu}}{\footnotesize{}
as shown in the slides.}{\footnotesize \par}
\item {\footnotesize{}Use naturality of }\texttt{\textcolor{blue}{\footnotesize{}pure}}{\footnotesize{}
to show that $\text{pure}\,f\odot\text{pure}\,g=\text{pure}\left(f\circ g\right)$}{\footnotesize \par}
\item {\footnotesize{}Show that $F^{A}\equiv\left(A\Rightarrow Z\right)\Rightarrow\left(1+A\right)$
is a functor but not applicative.}{\footnotesize \par}
\item {\footnotesize{}Show that $P^{S}$ is a monoid if $S$ is a monoid
and $P$ is any applicative functor, contrafunctor, or profunctor.}{\footnotesize \par}
\item {\footnotesize{}Implement an applicative instance for $F^{A}=1+\text{Int}\times A+A\times A\times A$.}{\footnotesize \par}
\item {\footnotesize{}Using applicative constructions, show without lengthy
proofs that $F^{A}=G^{A}+H^{G^{A}}$ is applicative if $G$ and $H$
are applicative functors.}{\footnotesize \par}
\item {\footnotesize{}Explicitly implement contrafunctor construction 2
and prove the laws.}{\footnotesize \par}
\item {\footnotesize{}For any contrafunctor $H^{A}$, construction 5 says
that $F^{A}\equiv H^{A}\Rightarrow A$ is applicative. Implement the
code of }\texttt{\textcolor{blue}{\footnotesize{}zip(fa, fb)}}{\footnotesize{}
for this construction.}{\footnotesize \par}
\item {\footnotesize{}Show that the recursive functor $F^{A}\equiv1+G^{A\times F^{A}}$
is applicative if $G^{A}$ is applicative and $\text{wu}_{F}$ is
defined recursively as $0+\text{pure}_{G}\left(1\times\text{wu}_{F}\right)$.}{\footnotesize \par}
\item {\footnotesize{}Explicitly implement profunctor construction 5 and
prove the laws. }{\footnotesize \par}
\item {\footnotesize{}Prove rigorously that all exponential-polynomial type
constructors are profunctors.}{\footnotesize \par}
\item {\footnotesize{}Implement profunctor and applicative instances for
$P^{A}\equiv A+Z\times G^{A}$ where $G^{A}$ is a given applicative
profunctor and $Z$ is a monoid.}{\footnotesize \par}
\item {\footnotesize{}Show that, for any profunctor $P^{A}$, one can implement
a function of type $A\Rightarrow P^{B}\Rightarrow P^{A\times B}$
but not of type $A\Rightarrow P^{B}\Rightarrow P^{A}$. }{\footnotesize \par}
\end{enumerate}
\end{frame}

\end{document}
